\tongjisetup{
  %******************************
  % 注意：
  %   1. 配置里面不要出现空行
  %   2. 不需要的配置信息可以删除
  %******************************
  %
  %=====
  % 秘级
  %=====
  secretlevel={保密},
  secretyear={2},
  %
  %=========
  % 中文信息
  %=========
  % 题目过长可以换行（推荐手动加入换行符，这样就可以控制换行的地方啦）。
  % ctitle={面向高可控、高可靠网络的网络编程\\与验证技术研究},
  % ctitle={网络协同应用编程与验证技术研究 \\ 网络验证与编程技术研究},
  % ctitle={面向高可靠、高适应性网络的网络验证与编程技术研究},
  ctitle={面向高可靠和高适应性网络的可验证路由\\编程体系研究},
  cheadingtitle={\TITLE},    %用于页眉的标题，不要换行
  cauthor={\hide{郭栋}},  
  studentnumber={\hide{1710350}},
  cmajorfirst={计算机科学与技术},
  cmajorsecond={网络与分布式计算},
  cdepartment={电子与信息工程学院},
  csupervisor={\hide{杨阳\ 教授}}, 
  % 如果没有副指导老师或者校外指导老师，把{}中内容留空即可，或者直接注释掉。
  cassosupervisor={}, % 副指导老师
  % 日期自动使用当前时间，若需手动指定，按如下方式修改：
  % cdate={\zhdigits{2018}年\zhnumber{11}月},
  % 没有基金的话就注释掉吧。
  % cfunds={},
  %
  %=========
  % 英文信息
  %=========
  % etitle={Network-Application Co-Programming and Verification}, 
  etitle={Research on Verifiable Routing Programming Architecture for Highly Reliable and Adaptive Networks}, 
  eauthor={\hide{Dong Guo}},
  emajorfirst={Engineering},
  emajorsecond={Computer Science and Technology},
  edepartment={Electronic and Information Engineering},
  % 日期自动使用当前时间，若需手动指定，按如下方式修改：
  % edate={November,\ 2018},
  % efunds={(Supported by the Natural Science Foundation of China for\\ Distinguished Young Scholars, Grant No.123456789)},    
  esupervisor={\hide{Prof. Y. Richard Yang}},
  % eassosupervisor={Prof. Gang Pei (XiaoWai)}
  }

% 定义中英文摘要和关键字
\begin{cabstract}  
  随着计算机网络向大规模、高带宽和应用多样性方向不断演进，现代网络面临着提高可靠性和传输需求适应性的一系列挑战。首先，网络的大规模和高带宽趋势意味着网络发生故障的可能性增加，以及网络故障带来的后果也会更加严重，例如金融交易和公共安全等领域都非常依赖网络的可靠性，即使是短暂的网络故障，也可能造成严重的社会和经济影响，所以，大规模高速网络对可靠性要求日益迫切，即网络需要能够持续提供正确且稳定的数据传输服务。另一方面，随着应用的多样性持续增长，不同类型的应用对网络的需求也表现出巨大的差异，例如，4K/8K视频和CDN服务对带宽的需求较高，而在线会议和视频直播等应用则对网络延迟有严格要求，这就要求网络具有传输需求适应性，即网络能够适应不同应用的需求，提供与应用需求一致的数据传输服务。因此，提高网络的可靠性和适应性是当前和未来计算机网络发展中的重要研究课题。

  然而，在网络可靠性和适应性领域尽管已经有大量的研究工作，但依然缺乏完整的具有可靠性和适应性保障的网络管理体系和基础工具。例如，数据平面验证被认为是目前保证网络可靠性的关键方法之一，然而现有的数据平面验证工具在大规模网络情况下需要数小时才能完成验证，对于现代高速网络来说是不可接受的。而在网络适应性方面，当前网络仍然采用尽力而为（Best effort）方式提供数据传输服务，网络被视为一种独立于应用的“黑盒”，应用只能通过历史数据被动地猜测网络的状态，导致其获取的网络信息是不可靠的，而且网络也无法根据应用的传输需求来调整其路由配置，使得网络的适应性难以得到实现。因此，如何实现完整的具有可靠性和适应性保障的网络管理体系依然是当前网络领域亟待解决的关键问题。


  本文提出了面向高可靠和高适应性网络的可验证路由编程体系研究，基于数据平面验证系统提供的可靠网络信息和快速验证能力，通过网络协同应用编程方式实现网络的高可靠和高适应性。首先，针对网络可靠性提出了面向大规模网络的数据平面验证系统Flash，Flash利用批处理和并行流水线执行实现大规模网络下的数据平面模型快速构建，并通过一致性提前验证方法CE2D实现增量式快速验证。其次，针对网络适应性提出了网络协同应用编程框架Socker和数据平面配置生成系统Fusion，在数据平面验证系统提供的可靠网络信息的基础上，从编程角度将网络控制和应用逻辑结合，并生成满足应用传输需求的数据平面配置。本文的主要贡献如下：

  \begin{enumerate}
    \item 提出并实现了首个面向大规模网络的数据平面验证系统Flash。针对大规模网络验证中的“更新风暴”现象，Flash通过快速逆模型变换FIMT（Fast Inverse Model Transformation）和并行流水线执行方法提高数据平面模型构建的吞吐量和伸缩性。同时，实现了首个面向大规模谓词操作的BDD库Nanobdd，解决了大规模网络数据平面验证中的谓词并发操作问题。在Facebook数据中心真实拓扑和开源数据集上的实验表明，Flash的数据平面构建速度相比已有工作提高了近40,000倍。
    \item 提出并实现了首个能够在不完整数据平面模型上实现一致性提前验证的方法CE2D（Consistent Efficient Early Detection）。针对大规模网络验证中存在的“长尾到达”现象，一致性提前验证方法首先构建一致性数据平面模型，然后基于递减图查询方法实现增量式快速验证。CE2D被设计为Flash的网络需求验证组件，在开源数据集和真实OpenR路由实例上的实验表明，相比已有工作的验证方法，能够将验证速度提高1,163倍。
    \item 提出并实现了首个套接字层的网络协同应用编程框架Socker。针对网络协同应用编程中的“网络与应用割裂”现象，Socker基于验证系统提供的可靠网络信息，从编程角度将网络控制和应用逻辑紧密结合，提出了声明式接口NQL（Network Query Language）和编程式接口实现网络协同应用的可验证路由编程过程。Socker通过套接字跟踪方法实现不同数据流和网络路由的绑定，并集成了基于ALTO和perfSONAR的路径可见性框架，实现了主动获取网络路径状态功能。实验结果表明，相比传统套接字编程，Socker实现了超过20\%的数据传输速度提升，并只有轻微的时间和内存开销。
    \item 实现了首个面向网络协同应用编程的数据平面配置生成系统Fusion。针对网络协同应用编程中的“路由冲突”现象，Fusion将数据平面配置生成问题建模为可满足性问题和整数规划问题，提出了基于定长编码和前缀编码的数据平面配置生成方法。相比于传统分配唯一路径标签方法，Fusion生成的数据平面配置的匹配域长度可降低75\%。
  \end{enumerate}

综上所述，本文通过设计实现面向大规模网络的数据平面验证系统以保障网络的可靠性，并基于验证系统创新性地提出网络协同编程框架以提高网络的传输需求适应性。相信通过本论文的研究，可以为未来网络向高可靠和高适应性方向演进提供有效的借鉴和参考。
  
\end{cabstract}

\ckeywords{网络可靠性, 网络验证, 数据平面验证, 网络协同应用}

\begin{eabstract}

As computer networks evolve towards largescale, high-bandwidth, and diverse application scenarios, modern networks face a series of challenges in enhancing reliability and adapting to varied transmission requirements. Firstly, the trends of network largescale and high bandwidth imply an increased likelihood of network failures, and the consequences of network failures will be more severe. Critical sectors such as financial transactions and public safety heavily rely on network reliability. Even brief network disruptions can lead to significant societal and economic impacts. Therefore, the urgent need for large-scale high-speed networks is to continuously provide reliable and stable data transmission services. On the other hand, with the continued growth of application diversity, different types of applications exhibit significant variations in their network requirements. For instance, 4K/8K videos and CDN services demand high bandwidth, while applications like online meetings and video streaming impose strict requirements on network latency. This necessitates network adaptability to transmission requirements, meaning that networks should accommodate the diverse needs of different applications, providing data transmission services consistent with their requirements. Consequently, enhancing network reliability and adaptability to transmission requirements stands as a crucial research topic in the current and future development of computer networks.

However, despite extensive research in the fields of network reliability and adaptability, there still lacks a comprehensive network routing management system and foundational tools with reliability assurance. For instance, data plane verification is considered one of the crucial methods for ensuring network reliability. However, existing data plane verification tools take hours to complete verification in large-scale network scenarios, which is unacceptable for modern high-speed networks. Regarding network adaptability, the current approach involves providing data transmission services on a best-effort basis. The network is treated as a "black box" independent of applications. Applications can only passively speculate about the network's status based on historical data, resulting in unreliable network information acquisition. Moreover, the network cannot adjust its routing configuration based on the transmission requirements of applications, making it challenging to achieve adaptability. Therefore, achieving a complete and reliable network routing management system remains a critical challenge in the current field of networking.

This dissertation presents a research initiative on a verifiable routing programming paradigm tailored for highly reliable and adaptable networks. Leveraging the reliable network information and rapid verification capabilities provided by the data plane verification system, the proposed approach achieves high reliability and adaptability through networking-application co-programming. Firstly, addressing network reliability, the dissertation presents Flash, a data plane verification system designed for large-scale networks. Flash utilizes batch processing and parallel pipeline execution to expedite the construction of data plane models in large-scale networks. It achieves rapid verification through the CE2D consistency check method, providing incremental and efficient verification. Secondly, to enhance network adaptability, the dissertation introduces Socker, a networking-application co-programming framework, and Fusion, a data plane configuration generation system. Building upon the reliable network information from the data plane verification system, Socker combines network control and application logic from a programming perspective. Fusion generates data plane configurations that meet the transmission requirements of applications. The primary contributions of this dissertation are as follows:

  \begin{enumerate}
    \item Introduce and implement the first data plane verification system, Flash, designed for large-scale networks. Addressing the challenge of "update storms" in large-scale network verification, Flash employs Fast Inverse Model Transformation (FIMT) and a parallel pipeline execution method to enhance the throughput and scalability of data plane model construction. Additionally, the implementation includes Nanobdd, the first Binary Decision Diagram (BDD) library tailored for large-scale predicate operations, addressing concurrency challenges in predicate operations during large-scale network data plane verification. Experiments conducted on real topologies from Facebook data centers and open-source datasets demonstrate that Flash achieves a nearly 40,000-fold improvement in data plane construction speed compared to existing approaches.
    \item Propose and implement the first consistency-efficient early detection method, CE2D (Consistent Efficient Early Detection), capable of operating on incomplete data plane models. Addressing the "long-tail arrivals" phenomenon in large-scale network verification, CE2D first constructs a consistent data plane model and then achieves incremental rapid verification through the decremental graph query method. CE2D is designed as a network requirement verification component of Flash. Experiments conducted on open-source datasets and real OpenR routing instances illustrate that Flash can enhance verification speeds by up to 1,163 times compared to existing verification methods.
    \item Propose and implement the first socket-layer network collaborative application programming framework, Socker. Addressing the "disconnection between network and application" phenomenon in network collaborative application programming, Socker tightly integrates network control and application logic from a programming perspective, leveraging reliable network information provided by the verification system. It introduces the Network Query Language (NQL) for declarative interactions and a programming interface to facilitate the verifiable route programming process for network collaborative applications. Socker employs a socket tracking method to bind different data streams and network routes and integrates a visibility framework based on ALTO and perfSONAR to actively acquire network path status. Experimental results demonstrate that, compared to traditional socket programming, Socker achieves over a 20\% improvement in data transmission speed with only minimal time and memory overhead.
    \item Implement the Fusion data plane configuration generation system, designed for network collaborative application programming. Addressing the "routing conflict" phenomenon in network collaborative application programming, Fusion models the data plane configuration generation problem as a satisfiability problem and an integer programming problem, introducing data plane configuration generation methods based on fixed-length encoding and prefix encoding. In comparison to traditional unique path labeling methods, Fusion reduces the matching domain length of generated data plane configurations by 75\%.
  \end{enumerate}

In summary, this dissertation designs and implements a data plane verification system for large-scale networks to ensure reliability. Additionally, it innovatively proposes a network collaborative programming framework based on the verification system to enhance the adaptability of network transmission requirements. It is believed that the research presented in this dissertation can provide valuable insights and references for the future development of networks towards high reliability and adaptability.

\end{eabstract}

\ekeywords{Network Reliability, Network Verification, Data Plane Verification, Network-application Integration}